\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$(?($\mathbb{N}\rightarrow$(IdLnk + Id)))), $v$:($i$:Id$\rightarrow$M($i$).(timed)state),\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$M($i$).state$\rightarrow$(?if $a$ $\in$ dom(M($i$).prob) then Outcome else Void fi )),
\\[0ex]${\it discrete}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$).
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ \=($\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\exists$\=$s$:M($i$).(timed)state\+
\\[0ex](\=$s$\+
\\[0ex]=
\\[0ex]if ($t$ =$_{0}$ 0)
\\[0ex]then $\lambda$$x$.M($i$).init($x$)?$v$($i$,$x$)
\\[0ex]else (CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))(($t$ {-} 1),$i$)).1
\\[0ex]fi 
\-\\[0ex]\& (\=(\=CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))($t$,$i$)\+\+
\\[0ex]=
\\[0ex]stutter{-}state($s$)
\\[0ex]$\in$ d{-}world{-}state($D$;$i$))
\-\\[0ex]$\vee$ ($\exists$\=$k$:Knd\+
\\[0ex]$\exists$\=${\it val}$:d{-}decl($D$;$i$)($k$)\+
\\[0ex](\=CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))($t$,$i$)\+
\\[0ex]=
\\[0ex]next{-}world{-}state($D$;$i$;$s$;$k$;${\it val}$)
\\[0ex]$\in$ d{-}world{-}state($D$;$i$))))))
\-\-\-\-\-\-
\end{tabbing}